package systemf;

import java.util.Objects;

/**
 * System F项（Term）
 * 支持变量、Lambda抽象、应用、类型抽象和类型应用
 */
public abstract class Term {
    
    /**
     * 变量
     */
    public static class Var extends Term {
        private final String name;
        
        public Var(String name) {
            this.name = name;
        }
        
        public String getName() {
            return name;
        }
        
        @Override
        public String toString() {
            return name;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            Var var = (Var) o;
            return Objects.equals(name, var.name);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(name);
        }
    }
    
    /**
     * Lambda抽象 λx:τ.M
     */
    public static class Lambda extends Term {
        private final String var;
        private final Type type;
        private final Term body;
        
        public Lambda(String var, Type type, Term body) {
            this.var = var;
            this.type = type;
            this.body = body;
        }
        
        public String getVar() {
            return var;
        }
        
        public Type getType() {
            return type;
        }
        
        public Term getBody() {
            return body;
        }
        
        @Override
        public String toString() {
            return "λ" + var + ":" + type + "." + body;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            Lambda lambda = (Lambda) o;
            return Objects.equals(var, lambda.var) &&
                   Objects.equals(type, lambda.type) &&
                   Objects.equals(body, lambda.body);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(var, type, body);
        }
    }
    
    /**
     * 应用 M N
     */
    public static class App extends Term {
        private final Term function;
        private final Term argument;
        
        public App(Term function, Term argument) {
            this.function = function;
            this.argument = argument;
        }
        
        public Term getFunction() {
            return function;
        }
        
        public Term getArgument() {
            return argument;
        }
        
        @Override
        public String toString() {
            String funcStr = (function instanceof Var || function instanceof Lambda || function instanceof TypeAbs)
                ? function.toString()
                : "(" + function + ")";
            String argStr = (argument instanceof Var || argument instanceof Lambda || argument instanceof TypeAbs)
                ? argument.toString()
                : "(" + argument + ")";
            return funcStr + " " + argStr;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            App app = (App) o;
            return Objects.equals(function, app.function) &&
                   Objects.equals(argument, app.argument);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(function, argument);
        }
    }
    
    /**
     * 类型抽象 Λα.M
     */
    public static class TypeAbs extends Term {
        private final String typeVar;
        private final Term body;
        
        public TypeAbs(String typeVar, Term body) {
            this.typeVar = typeVar;
            this.body = body;
        }
        
        public String getTypeVar() {
            return typeVar;
        }
        
        public Term getBody() {
            return body;
        }
        
        @Override
        public String toString() {
            return "Λ" + typeVar + "." + body;
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            TypeAbs typeAbs = (TypeAbs) o;
            return Objects.equals(typeVar, typeAbs.typeVar) &&
                   Objects.equals(body, typeAbs.body);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(typeVar, body);
        }
    }
    
    /**
     * 类型应用 M[τ]
     */
    public static class TypeApp extends Term {
        private final Term term;
        private final Type type;
        
        public TypeApp(Term term, Type type) {
            this.term = term;
            this.type = type;
        }
        
        public Term getTerm() {
            return term;
        }
        
        public Type getType() {
            return type;
        }
        
        @Override
        public String toString() {
            String termStr = (term instanceof Var || term instanceof Lambda || term instanceof TypeAbs)
                ? term.toString()
                : "(" + term + ")";
            return termStr + "[" + type + "]";
        }
        
        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            if (o == null || getClass() != o.getClass()) return false;
            TypeApp typeApp = (TypeApp) o;
            return Objects.equals(term, typeApp.term) &&
                   Objects.equals(type, typeApp.type);
        }
        
        @Override
        public int hashCode() {
            return Objects.hash(term, type);
        }
    }
    
    /**
     * 变量替换：将变量x替换为项N
     */
    public Term substitute(String var, Term replacement) {
        if (this instanceof Var) {
            Var v = (Var) this;
            return v.name.equals(var) ? replacement : this;
        } else if (this instanceof Lambda) {
            Lambda lambda = (Lambda) this;
            if (lambda.var.equals(var)) {
                return this; // 绑定变量，不替换
            }
            return new Lambda(
                lambda.var,
                lambda.type,
                lambda.body.substitute(var, replacement)
            );
        } else if (this instanceof App) {
            App app = (App) this;
            return new App(
                app.function.substitute(var, replacement),
                app.argument.substitute(var, replacement)
            );
        } else if (this instanceof TypeAbs) {
            TypeAbs typeAbs = (TypeAbs) this;
            return new TypeAbs(
                typeAbs.typeVar,
                typeAbs.body.substitute(var, replacement)
            );
        } else if (this instanceof TypeApp) {
            TypeApp typeApp = (TypeApp) this;
            return new TypeApp(
                typeApp.term.substitute(var, replacement),
                typeApp.type
            );
        }
        return this;
    }
}

